Tute (Week 7)

1. Abstract machines
2. Safety and Liveness
- 2.1. Decomposing Properties
- 2.2. Type Safety
3. Hindsight

1. Abstract machines

Recall the abstract machine from the Week 5 tutorial.

1.1. The E Machine

Evaluate the following expression using E-machine rules given in the lecture (where \(\mathtt{Num}\) is abbreviated to \(\mathtt{N}\)):

\[\small (\mathtt{Apply}\ (\mathtt{Fun}\ (f.x. \mathtt{If}\ (\mathtt{Less}\ x\ (\mathtt{N}\ 2))\ (\mathtt{N}\ 0)\ (\mathtt{Apply}\ f\ (\mathtt{Minus}\ x\ (\mathtt{N}\ 1)))))\ (\mathtt{N}\ 3))\]

You don't need to write down every single step, but show how the contents of the stack and environments change during evaluation.

1.2. Closures

Give an example of a program that evaluates to different results in an environment semantics, depending on whether or not closures are used. You may use the MinHS dialect used in your assignment.

1.3. Tail Calls

Consider the following two programs:

sumInt :: Int -> Int
sumInt 0 = 0
sumInt n = n + (sumInt (n-1))

sumInt' :: Int -> Int
sumInt' n = sum2 0 n
  where
    sum2 m 0 = m
    sum2 m n = sum2 (m+n) (n-1)

In a strict (call-by-value) language, the first program would lead to a stack overflow if applied to a sufficiently large number, but the second would not.

Explain how tail-call elimination can be applied to these examples.
How can we change the definition of our E-Machine to optimize tail-calls?
In Haskell, the second version will still exhaust all available memory if applied to a sufficiently large number. Why is this the case?

2. Safety and Liveness

a) Type Safety is said to be a safety property, and termination is said to be a liveness property. Suppose I was impatient, and stated a stronger termination property as follows:

The process will terminate and halt execution within a billion steps.

Is this version still a liveness property?

b) What are the properties of progress and preservation? Are they safety or liveness properties?

2.1. Decomposing Properties

For each of the following program properties, decompose it into the intersection of a safety property and a liveness property.

The program will allocate exactly 100MB of memory.
The program will not overflow the stack.
The program will return the sum of its inputs.
The program will call the function foo.

2.2. Type Safety

Why is the handling of partial functions important for a type safe language? How does it impact progress and preservation?

3. Hindsight

This question is about the hindsight language from Assignment 1.

Write a recursive hindsight function (recfun expression) with type Int -> F Int, that computes the n:th triangular number. C.f. the sumInt Haskell function above
Now consider the auxiliary sum2 function above. If we transcribe this into a hindsight function of type Int -> Int -> F Int we will be unable to mimic the evaluation order used by Haskell. Why? And what type signature would we use if we wanted to mimic the Haskell evaluation?
When we came up with hindsight, by far the most contentious issue was the treatment of Cons. It's a bit annoying that you have to force it. Why do you think it is the way it is? What are the alternatives?